Integrated circuits have become increasingly prevalent in today's society. The number of digital systems that include integrated circuits continues to steadily increase and may be driven by a wide array of products and systems. Added functionalities may be provided to integrated circuits in order to execute additional tasks or to effectuate more sophisticated operations in their respective applications or environments. Additionally, system parameters of integrated circuits may dictate that their operations be performed in an optimal time interval, which allows for even more operations to be accommodated in a given clock cycle. These rigorous demands associated with production and design generally result in the need for more advanced and complex verification processes and procedures.
Verification techniques are generally implemented in order to ensure that an integrated circuit or a digital element is capable of performing its intended functionality. In other cases, verification techniques may be used in order to ascertain whether a selected characteristic, behavior, or property is present in a given target circuit. Flaws or inaccuracies in an integrated circuit or a digital element may inhibit system functionality and/or cause significant operational problems in a corresponding architecture.
In integrated circuit and other digital applications, a reachability analysis poses a significant problem. A reachability analysis may include a conjunction phase and a quantification phase that cooperate in order to produce an image computation for a reachability analysis in a given circuit. Either of these phases may present significant obstacles during operations. For example, graphs may become excessively large or ‘blowup’ during a given analysis. Such a blowup is impractical for system designers because it may generate a host of time intensive activities or tasks. Additionally, such a result may not be feasible to evaluate because it forces a designer to exhaustively investigate the blowup to ensure correctness or accuracy associated with that portion of a target circuit. Accordingly, the ability to verify or validate a design for any integrated circuit or digital element presents a significant challenge to digital system designers and integrated circuit manufacturers.